package org.xteam.sled.semantic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Stack;

import org.xteam.parser.runtime.Span;
import org.xteam.sled.ast.AndPattern;
import org.xteam.sled.ast.BinaryPattern;
import org.xteam.sled.ast.CallPattern;
import org.xteam.sled.ast.DefaultSledVisitor;
import org.xteam.sled.ast.EpsilonPattern;
import org.xteam.sled.ast.EqOp;
import org.xteam.sled.ast.GeneratorPattern;
import org.xteam.sled.ast.Ident;
import org.xteam.sled.ast.LabelPattern;
import org.xteam.sled.ast.ListPattern;
import org.xteam.sled.ast.OrPattern;
import org.xteam.sled.ast.PatternIdent;
import org.xteam.sled.ast.PrefixPattern;
import org.xteam.sled.ast.RelationPattern;
import org.xteam.sled.ast.Relop;
import org.xteam.sled.ast.SequentPattern;
import org.xteam.sled.ast.SuffixPattern;
import org.xteam.sled.model.ILabelledSequent;
import org.xteam.sled.model.LabelledDisjunct;
import org.xteam.sled.model.LabelledPattern;
import org.xteam.sled.model.LabelledSequence;
import org.xteam.sled.model.ActualLabel;
import org.xteam.sled.model.RangeConstraint;
import org.xteam.sled.semantic.exp.Exp;
import org.xteam.sled.semantic.exp.ExpConst;


public class PatternSemantic extends DefaultSledVisitor {
	
	public static abstract class Result<T> {
		public boolean isError() {
			return false;
		}

		public boolean isSingle() {
			return false;
		}

		public Result<T> combine(Result<T> right, IBinaryFunc<T> func) {
			return new Error<T>();
		}

		public Result<T> combineWithSingle(Single<T> single, IBinaryFunc<T> func) {
			return new Error<T>();
		}

		public Result<T> combineWithGroup(Group<T> group, IBinaryFunc<T> func) {
			return new Error<T>();
		}

		public Result<T> apply(IUnaryFunc<T> unaryFunc) {
			return new Error<T>();
		}
		
	}
	
	public static class Error<T> extends Result<T> {
		public boolean isError() {
			return true;
		}
	}
	
	public static class Single<T> extends Result<T> {
		T pattern;
		public Single(T pattern) {
			this.pattern = pattern;
		}
		public boolean isSingle() {
			return true;
		}
		
		@Override
		public Result<T> combine(Result<T> right, IBinaryFunc<T> func) {
			return right.combineWithSingle(this, func);
		}
		
		public Result<T> combineWithSingle(Single<T> left, IBinaryFunc<T> func) {
			return new Single<T>(func.exec(left.pattern, pattern));
		}

		public Result<T> combineWithGroup(Group<T> group, IBinaryFunc<T> func) {
			Group<T> res = new Group<T>();
			for (T left : group.patterns) {
				res.patterns.add(func.exec(left, pattern));
			}
			return res;
		}
		
		public Result<T> apply(IUnaryFunc<T> func) {
			return new Single<T>(func.apply(pattern));
		}
	}
	
	public static class Group<T> extends Result<T> {
		List<T> patterns = new ArrayList<T>();
		
		public Group() {
			this(new ArrayList<T>());
		}

		public Group(List<T> t) {
			this.patterns = t;
		}

		@Override
		public Result<T> combine(Result<T> right, IBinaryFunc<T> func) {
			return right.combineWithGroup(this, func);
		}
		
		public Result<T> combineWithSingle(Single<T> left, IBinaryFunc<T> func) {
			Group<T> res = new Group<T>();
			for (T right : patterns) {
				res.patterns.add(func.exec(left.pattern, right));
			}
			return res;
		}

		public Result<T> combineWithGroup(Group<T> left, IBinaryFunc<T> func) {
			Group<T> res = new Group<T>();
			for (T l : left.patterns) {
				for (T r : patterns) {
					res.patterns.add(func.exec(l, r));
				}
			}
			return res;
		}
		
		public Result<T> apply(IUnaryFunc<T> func) {
			Group<T> res = new Group<T>();
			for (T right : patterns) {
				res.patterns.add(func.apply(right));
			}
			return res;
		}
	}
	
	// app (A.SOME_token, [e]) = emap (SINGLE o Pattern.wildcard) (lookupToken e)
	// app (A.LIST, es)   = emap (GROUP o single) (elabPats es)
	
	// elabPat (A.INT n)               = error "integer literal"
	// elabPat (A.LITERAL_exp s)       = error "string literal"
	// app (A.GEN_to, es) = error "expected pattern; found generating expression"
	// app (A.PLUS,  es) = error "expected pattern; found integer expression"
	// app (A.MINUS, es) = error "expected pattern; found integer expression"
	// app (A.TIMES, es) = error "expected pattern; found integer expression"
	// app (A.DIV,   es) = error "expected pattern; found integer expression"
	// app (A.SLICE, es)    = error "expected pattern; found integer expression"
	// app (A.EXTEND, es)   = error "expected pattern; found integer expression"
	// app (A.WILDCARD, es) = error "expected pattern; found integer expression"
	
	private IEvaluationContext context;
	private Stack<Result<LabelledPattern>> stack = new Stack<Result<LabelledPattern>>();
	
	public PatternSemantic(IEvaluationContext context) {
		this.context = context;
	}
	
	public boolean hasError() {
		return stack.peek().isError();
	}
	
	// val elabPat = gemap (Pattern.subst (simplify o eliminateInstances)) o elabPat

	public List<LabelledPattern> getPatternList() {
		if (stack.peek().isError() || stack.peek().isSingle())
			return null;
		List<LabelledPattern> res = new ArrayList<LabelledPattern>();
		for (LabelledPattern p : ((Group<LabelledPattern>)stack.peek()).patterns) {
			res.add(p.subst(new EliminateInstance()));
		}
		return res;
	}
	
	public LabelledPattern getPattern() {
		if (stack.peek().isError() || ! stack.peek().isSingle())
			return null;
		return ((Single<LabelledPattern>)stack.peek()).pattern.subst(new EliminateInstance());
	}
	
	private void push(Result<LabelledPattern> result) {
		stack.push(result);
	}
	
	private Result<LabelledPattern> pop() {
		return stack.pop();
	}
	
	// app (A.OR, es)     = gemap Pattern.orp  (elabPats es)
	public void visitOrPattern(OrPattern orPattern) {
		visitBinary(orPattern, new IBinaryFunc<LabelledPattern>() {
			public LabelledPattern exec(LabelledPattern left, LabelledPattern right) {
				return left.or(right);
			}
		});
	}
	
	// app (A.AND, es)    = gemap Pattern.andp (elabPats es)
	public void visitAndPattern(AndPattern andPattern) {
		visitBinary(andPattern, new IBinaryFunc<LabelledPattern>() {
			public LabelledPattern exec(LabelledPattern left, LabelledPattern right) {
				return left.and(right);
			}
		});
	}
	
	// app (A.CONCAT, es) = gemap Pattern.seqp (elabPats es)
	public void visitSequentPattern(SequentPattern sequentPattern) {
		visitBinary(sequentPattern, new IBinaryFunc<LabelledPattern>() {
			public LabelledPattern exec(LabelledPattern left, LabelledPattern right) {
				return left.seq(right);
			}
		});
	}
	
	// app (A.PLABEL l, []) = (OK o SINGLE o Patterns.actualLabel) l
	public void visitLabelPattern(LabelPattern aLabelPattern) {
		List<ILabelledSequent> seq = new ArrayList<ILabelledSequent>();
		seq.add(ActualLabel.newLabel(aLabelPattern.getIdent().getName()));
		final LabelledPattern p = new LabelledPattern(new LabelledDisjunct(new LabelledSequence(seq)));
		aLabelPattern.getExpr().visit(this);
		Result<LabelledPattern> r = pop();
		if (r.isError())
			push(new Error<LabelledPattern>());
		else {
			push(r.apply(new IUnaryFunc<LabelledPattern>() {
				public LabelledPattern apply(LabelledPattern pattern) {
					return p.seq(pattern);
				}
			}));
		}
	}
	
	public void visitListPattern(ListPattern aListPattern) {
		List<Result<LabelledPattern>> res = new ArrayList<Result<LabelledPattern>>();
		for (Ident e : aListPattern.getNames()) {
			doIdent(e.getName(), e.span());
			res.add(stack.pop());
		}
		Result<List<LabelledPattern>> r = lifo(res);
		if (r.isError() || ! r.isSingle())
			stack.push(new Error<LabelledPattern>());
		else
			stack.push(new Group<LabelledPattern>(((Single<List<LabelledPattern>>)r).pattern));
	}
	
	private Result<List<LabelledPattern>> lifo(List<Result<LabelledPattern>> res) {
		Result<List<LabelledPattern>> t = new Single<List<LabelledPattern>>(new ArrayList<LabelledPattern>());
		for (Result<LabelledPattern> r : res) {
			if (r.isError()) {
				return new Error<List<LabelledPattern>>();
			} else if (r.isSingle()) {
				t = add(t, ((Single<LabelledPattern>)r).pattern);
			} else {
				t = cross(t, ((Group<LabelledPattern>)r).patterns);
			}
		}
		return t;
	}

	private Result<List<LabelledPattern>> add(Result<List<LabelledPattern>> t,
			LabelledPattern pattern) {
		if (t.isSingle()) {
			List<LabelledPattern> e = new ArrayList<LabelledPattern>(((Single<List<LabelledPattern>>)t).pattern);
			e.add(pattern);
			return new Single<List<LabelledPattern>>(e);
		}
		List<List<LabelledPattern>> r = new ArrayList<List<LabelledPattern>>();
		for (List<LabelledPattern> e : ((Group<List<LabelledPattern>>)t).patterns) {
			e = new ArrayList<LabelledPattern>(e);
			e.add(pattern);
			r.add(e);
		}
		return new Group<List<LabelledPattern>>(r);
	}
	
	private Result<List<LabelledPattern>> cross(
			Result<List<LabelledPattern>> t, List<LabelledPattern> patterns) {
		if (t.isSingle()) {
			throw new RuntimeException();
		}
		throw new RuntimeException();
	}

	public void visitEpsilonPattern(EpsilonPattern aEpsilonPattern) {
		doIdent("epsilon", aEpsilonPattern.span());
	}
	
	// app (A.PREFIX_DOTS,  [e]) = gemap Pattern.preDots  (elabPat e)
	public void visitPrefixPattern(PrefixPattern prefixPattern) {
		prefixPattern.getExpr().visit(this);
		Result<LabelledPattern> left = pop();
		if (left.isError()) 
			push(new Error<LabelledPattern>());
		else {
			push(left.apply(new IUnaryFunc<LabelledPattern>() {
				public LabelledPattern apply(LabelledPattern pattern) {
					return pattern.preDots();
				}
			}));
		}
	}
	
	// app (A.POSTFIX_DOTS, [e]) = gemap Pattern.postDots (elabPat e)
	public void visitSuffixPattern(SuffixPattern suffixPattern) {
		suffixPattern.getExpr().visit(this);
		Result<LabelledPattern> left = pop();
		if (left.isError()) 
			push(new Error<LabelledPattern>());
		else {
			push(left.apply(new IUnaryFunc<LabelledPattern>() {
				public LabelledPattern apply(LabelledPattern pattern) {
					return pattern.postDots();
				}
			}));
		}
	}
	
	private void visitBinary(BinaryPattern pattern, IBinaryFunc<LabelledPattern> func) {
		pattern.getLeft().visit(this);
		Result<LabelledPattern> left = pop();
		pattern.getRight().visit(this);
		Result<LabelledPattern> right = pop();
		if (left.isError() || right.isError()) 
			push(new Error<LabelledPattern>());
		else {
			push(left.combine(right, func));
		}
	}
	
	// fun lookupPat name = emap Denotable.projectPattern (lookup name)
	// elabPat (A.IDENT id)            = emap SINGLE (lookupPat id)
	public void visitPatternIdent(PatternIdent patternIdent) {
		doIdent(patternIdent.getIdent().getName(), patternIdent.span());
	}
	
	private void doIdent(String name, Span span) {
		IDenotable denotable = context.lookup(name, span);
		LabelledPattern p;
		if (denotable == null || (p = (LabelledPattern)denotable.projectPattern(context, span)) == null)
			push(new Error<LabelledPattern>());
		else
			push(new Single<LabelledPattern>(p));
	}
	
	// app (A.RELOP rel, [left, right]) =  strip (emap (groupErrors o (gmap (constraint (left, rel)))) (elabInt right))
	public void visitGeneratorPattern(GeneratorPattern generatorPattern) {
		push(buildListContraints(generatorPattern.span(),
				generatorPattern.getIdent(), generatorPattern.getRelop(),
				(new GeneratorIntegerSemantic(context)).analyse(generatorPattern.getGenerator())));
	}

	// app (A.RELOP rel, [left, right]) =  strip (emap (groupErrors o (gmap (constraint (left, rel)))) (elabInt right))
	public void visitRelationPattern(RelationPattern relationPattern) {
		push(buildContraints(relationPattern.span(),
				relationPattern.getIdent(), relationPattern.getRelop(),
				(new IntegerSemantic(context)).analyse(relationPattern.getExpr())));
	}
	
	// elabPat (A.APP x)               = constructorApp x
	public void visitCallPattern(CallPattern aCallPattern) {
		List<OpcodeElement> opcodes = context.explodeOpcode(aCallPattern.getOpcode());
		LabelledPattern p = null;
		for (OpcodeElement opcode : opcodes) {
			InstructionConstructor iconst = context.lookupConstructor(opcode.name(), aCallPattern.getOpcode().span());
			LabelledPattern pat = iconst.apply(aCallPattern.getArguments(), aCallPattern.span(), context /*, free_env */);
			p = p == null ? pat : p.or(pat);
		}
		push(new Single<LabelledPattern>(p));
	}
	
	private Result<LabelledPattern> buildListContraints(Span span, Ident ident, Relop relop, List<ExpConst> x) {
		Group<LabelledPattern> g = new Group<LabelledPattern>();
		for (ExpConst e : x) {
			LabelledPattern pattern = constraint(context, span, ident, relop, e);
			if (pattern == null)
				return new Error<LabelledPattern>();
			g.patterns.add(pattern);
		}
		return g;
	}
	
	private Result<LabelledPattern> buildContraints(Span span, Ident ident, Relop relop, Exp x) {
		LabelledPattern p = constraint(context, span, ident, relop, x);
		return p == null ? new Error<LabelledPattern>() : new Single<LabelledPattern>(p);
	}

	public static LabelledPattern constraint (IEvaluationContext context, Span span, Ident left, Relop relop, Exp intExp) {
		IDenotable denotable = context.lookup(left.getName(), left.span());
		if (denotable != null) {
			if (denotable instanceof Field) {
				Field field = (Field) denotable;
				return LabelledPattern.constraint(context, span, field, relop, intExp);
			} else {
				context.reportError(left.span(), left.getName()
						+ " is not a field");
			}
		}
		return null;
	}

}
